1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import geometry.manifold.smooth_manifold_with_corners linear_algebra.finite_dimensional
src         └────────────────────────────────────────────┘ └───────────────────────────────┘
  8  
  9  /-!
 10  # Constructing examples of manifolds over ℝ
 11  
 12  We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless
 13  or with boundary or with corners. As a concrete example, we construct explicitly the manifold with
 14  boundary structure on the real interval [x, y].
 15  
 16  More specifically, we introduce
 17  * `euclidean_space n` for a model vector space of dimension `n`.
 18  * `model_with_corners ℝ (euclidean_space n) (euclidean_half_space n)` for the model space used
 19  to define `n`-dimensional real manifolds with boundary
 20  * `model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n)` for the model space used
 21  to define `n`-dimensional real manifolds with corners
 22  
 23  ## Implementation notes
 24  
 25  The manifold structure on the interval [x, y] = Icc x y requires the assumption `x < y`. We
 26  introduce a dummy class `lt_class x y` for this, to make such an assumption available to typeclass
 27  search. This should hopefully not be necessary any more in Lean 4.
 28  -/
 29  
 30  noncomputable theory
 31  open set
 32  
 33  /--
 34  The space ℝ^n. Note that the name is slightly misleading, as we only need a normed space
 35  structure on ℝ^n, but the one we use here is the sup norm and not the euclidean one -- this is not
 36  a problem for the manifold applications, but should probably be refactored at some point.
 37  -/
 38  def euclidean_space (n : ℕ) : Type := (fin n → ℝ)
id                                         └─┘    
src                                        └─┘     
typ                                        └─┘    
 39  
 40  /--
 41  The half-space in ℝ^n, used to model manifolds with boundary. We only define it when `1 ≤ n`, as the
 42  definition only makes sense in this case.
 43  -/
 44  def euclidean_half_space (n : ℕ) [has_zero (fin n)] : Type :=
id                                    └──────┘  └─┘ 
src                                   └──────┘  └─┘
typ                                   └──────┘  └─┘ 
 45  {x : euclidean_space n // 0 ≤ x 0}
id       └─────────────┘        
src      └─────────────┘        
typ      └─────────────┘        
doc       └─────────────┘
 46  
 47  /--
 48  The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative
 49  coordinates.
 50  -/
 51  def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space n // ∀i:fin n, 0 ≤ x i}
id                                               └─────────────┘        └─┘       
src                                              └─────────────┘         └─┘      
typ                                              └─────────────┘        └─┘       
doc                                                └─────────────┘
 52  
 53  section
 54  /- Register class instances for euclidean space and half-space and quadrant -/
 55  local attribute [reducible] euclidean_space euclidean_half_space euclidean_quadrant
id                               └─────────────┘ └──────────────────┘ └────────────────┘
src                              └─────────────┘ └──────────────────┘ └────────────────┘
typ                              └─────────────┘ └──────────────────┘ └────────────────┘
doc                   └───────┘  └─────────────┘ └──────────────────┘ └────────────────┘
 56  variable {n : ℕ}
id                 
src                
typ                
 57  
 58   -- short-circuit type class inference
 59  instance : vector_space ℝ (euclidean_space n) := by apply_instance
id              └──────────┘   └─────────────┘ 
src             └──────────┘   └─────────────┘          └─────────────┘
typ             └──────────┘   └─────────────┘         └─────────────┘
doc             └──────────┘    └─────────────┘          └─────────────┘
txt                                                      └─────────────┘
par                                                      └─────────────┘
pid                                                                    
st                                                      └──────────────┘
 60  instance : normed_group (euclidean_space n) := by apply_instance
id              └──────────┘  └─────────────┘ 
src             └──────────┘  └─────────────┘          └─────────────┘
typ             └──────────┘  └─────────────┘         └─────────────┘
doc             └──────────┘  └─────────────┘          └─────────────┘
txt                                                    └─────────────┘
par                                                    └─────────────┘
pid                                                                  
st                                                    └──────────────┘
 61  instance : normed_space ℝ (euclidean_space n) := by apply_instance
id              └──────────┘   └─────────────┘ 
src             └──────────┘   └─────────────┘          └─────────────┘
typ             └──────────┘   └─────────────┘         └─────────────┘
doc             └──────────┘    └─────────────┘          └─────────────┘
txt                                                      └─────────────┘
par                                                      └─────────────┘
pid                                                                    
st                                                      └──────────────┘
 62  instance [has_zero (fin n)] : topological_space (euclidean_half_space n) := by apply_instance
id             └──────┘  └─┘      └───────────────┘  └──────────────────┘ 
src            └──────┘  └─┘       └───────────────┘  └──────────────────┘          └─────────────┘
typ            └──────┘  └─┘      └───────────────┘  └──────────────────┘         └─────────────┘
doc                                └───────────────┘  └──────────────────┘          └─────────────┘
txt                                                                                 └─────────────┘
par                                                                                 └─────────────┘
pid                                                                                               
st                                                                                 └──────────────┘
 63  instance : topological_space (euclidean_quadrant n) := by apply_instance
id              └───────────────┘  └────────────────┘ 
src             └───────────────┘  └────────────────┘          └─────────────┘
typ             └───────────────┘  └────────────────┘         └─────────────┘
doc             └───────────────┘  └────────────────┘          └─────────────┘
txt                                                            └─────────────┘
par                                                            └─────────────┘
pid                                                                          
st                                                            └──────────────┘
 64  instance : finite_dimensional ℝ (euclidean_space n) := by apply_instance
id              └────────────────┘   └─────────────┘ 
src             └────────────────┘   └─────────────┘          └──────────────
typ             └────────────────┘   └─────────────┘         └──────────────
doc             └────────────────┘    └─────────────┘          └──────────────
txt                                                            └──────────────
par                                                            └──────────────
pid                                                                          
st                                                            └───────────────
 65  
src  
typ  
doc  
txt  
par  
pid  
st   
 66  @[simp] lemma findim_euclidean_space : finite_dimensional.findim ℝ (euclidean_space n) = n :=
id                                          └───────────────────────┘   └─────────────┘    
src                                         └───────────────────────┘   └─────────────┘    
typ                                         └───────────────────────┘   └─────────────┘    
doc    └──┘                                 └───────────────────────┘    └─────────────┘
 67  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
 68  
src  
typ  
doc  
txt  
par  
pid  
 69  lemma range_half_space (n : ℕ) [has_zero (fin n)] :
 70    range (λx : euclidean_half_space n, x.val) = {y | 0 ≤ y 0 } :=
 71  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
 72  
src  
typ  
doc  
txt  
par  
pid  
 73  lemma range_quadrant (n : ℕ) :
 74    range (λx : euclidean_quadrant n, x.val) = {y | ∀i:fin n, 0 ≤ y i } :=
 75  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
 76  
src  
typ  
doc  
txt  
par  
pid  
 77  end
 78  
 79  /--
 80  Definition of the model with corners (euclidean_space n, euclidean_half_space n), used as a
 81  model for manifolds with boundary.
 82  -/
 83  def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
 84    model_with_corners ℝ (euclidean_space n) (euclidean_half_space n) :=
 85  { to_fun     := λx, x.val,
 86    inv_fun    := λx, ⟨λi, if h : i = 0 then max (x i) 0 else x i, by simp [le_refl]⟩,
src                                                                      └────┘       
typ                                                                      └────┘       
doc                                                                      └────┘       
txt                                                                      └────┘       
par                                                                      └────┘       
pid                                                                                 
 87    source     := univ,
 88    target     := range (λx : euclidean_half_space n, x.val),
 89    map_source := λx hx, by simpa [-mem_range, mem_range_self] using x.property,
src                            └─────────────────┘              └──────┘
typ                            └─────────────────┘              └──────┘
doc                            └─────────────────┘              └──────┘
txt                            └─────────────────┘              └──────┘
par                            └─────────────────┘              └──────┘
pid                                 └───────────┘              └────┘
 90    map_target := λx hx, mem_univ _,
 91    left_inv   := λ⟨xval, xprop⟩ hx, begin
 92      rw subtype.mk_eq_mk,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st        └────────────────┘└─
 93      ext1 i,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid          └┘
st   ─────────┘└─
 94      by_cases hi : i = 0;
id                      
src      └───────┘  └─┘ └┘
typ      └───────┘  └─┘└┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ─────────────────────────
 95      simp [hi, xprop]
id             └┘  └───┘
src      └────┘  └┘     └─
typ      └────┘└┘└┘└───┘└─
doc      └────┘  └┘     └─
txt      └────┘  └┘     └─
par      └────┘  └┘     └─
pid            └┘     
st   ─────────────────────
 96    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 97    right_inv := λx hx, begin
id                    └┘
typ                   └┘
st                         └─────
 98      simp [range_half_space] at hx,
id             └──────────────┘
src      └────┘└──────────────┘└─────┘
typ      └────┘└──────────────┘└─────┘
doc      └────┘                └─────┘
txt      └────┘                └─────┘
par      └────┘                └─────┘
pid                          └───┘
st   ────────────────────────────────┘└─
 99      ext1 i,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid          └┘
st   ─────────┘└─
100      by_cases hi : i = 0;
id                     
src      └───────┘  └─┘  └┘
typ      └───────┘  └─┘ └┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ─────────────────────────
101      simp [hi, hx]
id             └┘  └┘
src      └────┘  └┘  └─
typ      └────┘└┘└┘└┘└─
doc      └────┘  └┘  └─
txt      └────┘  └┘  └─
par      └────┘  └┘  └─
pid            └┘  
st   ──────────────────
102    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
103    source_eq   := rfl,
id                    └─┘
src                   └─┘
typ                   └─┘
104    unique_diff := begin
st                    └─────
105      /- To check that the half-space has the unique differentiability property, we use the criterion
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
106      `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
107      rw range_half_space,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────┘└─
108      apply unique_diff_on_convex,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘└───────────────────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
109      show convex {y : euclidean_space n | 0 ≤ y 0},
id            └────┘     └─────────────┘      
src      └───┘└────┘└──┘└─────────────┘ └───┘ └─┘
typ      └───┘└────┘└──┘└─────────────┘└───┘ └─┘
doc      └───┘└────┘ └──┘└─────────────┘ └───┘  └─┘
txt      └───┘       └──┘                └───┘  └─┘
par      └───┘       └──┘                └───┘  └─┘
pid      └───┘       └──┘                └───┘  └─┘
st   ────────────────────────────────────────────────┘└─
110      { assume x y hx hy a b ha hb hab,
src        └────────────────────────────┘
typ        └────────────────────────────┘
doc        └────────────────────────────┘
txt        └────────────────────────────┘
par        └────────────────────────────┘
pid        └────────────────────────────┘
st   ─────┘└────────────────────────────┘└─
111        simpa using add_le_add (mul_nonneg' ha hx) (mul_nonneg' hb hy) },
id                     └────────┘              └┘ └┘   └─────────┘ └┘ └┘
src        └──────────┘└────────┘                └┘ └─────────┘    └┘
typ        └──────────┘└────────┘            └┘└┘└┘ └─────────┘└┘└┘└┘
doc        └──────────┘                          └┘                └┘
txt        └──────────┘                          └┘                └┘
par        └──────────┘                          └┘                └┘
pid             └────┘                          └┘                
st   ────────────────────────────────────────────────────────────────────┘└┘
112      show (interior {y : euclidean_space n | 0 ≤ y 0}).nonempty,
id             └──────┘     └─────────────┘ 
src      └───┘ └──────┘└──┘└─────────────┘ └───┘  └───────────┘
typ      └───┘ └──────┘└──┘└─────────────┘└───┘  └───────────┘
doc      └───┘ └──────┘ └──┘└─────────────┘ └───┘  └───────────┘
txt      └───┘          └──┘                └───┘  └───────────┘
par      └───┘          └──┘                └───┘  └───────────┘
pid      └───┘          └──┘                └───┘  └──────────┘
st   ────────────────────────────────────────────────────────────────
113      { use (λi, 1),
src        └──┘  └───┘
typ        └──┘  └───┘
doc        └──┘  └───┘
txt        └──┘  └───┘
par        └──┘  └───┘
pid             └───┘
st   ────────────────┘└─
114        rw mem_interior,
id            └──────────┘
src        └─┘└──────────┘
typ        └─┘└──────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────────────┘└─
115        refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,
id                  └┘  └──┘        └─┘          └─┘     └─┘
src        └─────┘  └┘ └──┘└─┘    └─┘ └─┘  └─┘ └─┘└───┘└─┘ └───────
typ        └─────┘  └┘ └──┘└─┘    └─┘└─┘  └─┘ └─┘└───┘└─┘ └───────
doc        └─────┘  └┘     └─┘        └─┘  └─┘ └─┘└───┘    └───────
txt        └─────┘         └─┘        └─┘  └─┘    └───┘    └───────
par        └─────┘         └─┘        └─┘  └─┘    └───┘    └───────
pid                       └─┘        └─┘  └─┘    └───┘    └───────
st   ──────────────────────────────────────────────────────────────────
116          is_open_set_pi finite_univ (λa ha, is_open_Ioi), _⟩,
id           └────────────┘ └─────────┘         └─────────┘
src  ───────┘└────────────┘└─────────┘  └────┘└─────────┘└───┘
typ  ───────┘└────────────┘└─────────┘  └────┘└─────────┘└───┘
doc  ───────┘                           └────┘           └───┘
txt  ───────┘                           └────┘           └───┘
par  ───────┘                           └────┘           └───┘
pid  ───────┘                           └────┘           └───┘
st   ──────────────────────────────────────────────────────────┘└─
117        { assume x hx,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ───────┘└─────────┘└─
118          simp [pi] at hx,
id                 └┘
src          └────┘└┘└─────┘
typ          └────┘└┘└─────┘
doc          └────┘└┘└─────┘
txt          └────┘  └─────┘
par          └────┘  └─────┘
pid                └───┘
st   ──────────────────────┘└─
119          exact le_of_lt (hx 0) },
id                 └──────┘  └┘
src          └────┘└──────┘   └──┘
typ          └────┘└──────┘ └┘└──┘
doc          └────┘           └──┘
txt          └────┘           └──┘
par          └────┘           └──┘
pid                          └─┘
st   ─────────────────────────────┘└┘
120        { simp only [pi, forall_prop_of_true, mem_univ, mem_Ioi],
id                      └┘  └─────────────────┘  └──────┘  └─────┘
src          └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘
typ          └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘
doc          └─────────┘└┘└┘                   └┘        └┘       
txt          └─────────┘  └┘                   └┘        └┘       
par          └─────────┘  └┘                   └┘        └┘       
pid              └──┘└┘  └┘                   └┘        └┘       
st   ─────────────────────────────────────────────────────────────┘└─
121          assume i,
src          └──────┘
typ          └──────┘
doc          └──────┘
txt          └──────┘
par          └──────┘
pid          └──────┘
st   ───────────────┘└─
122          exact zero_lt_one } }
id                 └─────────┘
src          └────┘└─────────┘
typ          └────┘└─────────┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                          
st   ─────────────────────────┘└───
123    end,
st   ────┘
124    continuous_to_fun  := continuous_subtype_val,
id                           └────────────────────┘
src                          └────────────────────┘
typ                          └────────────────────┘
125    continuous_inv_fun := begin
st                           └─────
126      apply continuous_subtype_mk,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
127      apply continuous_pi,
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────┘└─
128      assume i,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
129      by_cases h : i = 0,
id                    
src      └───────┘ └─┘  └┘
typ      └───────┘ └─┘ └┘
doc      └───────┘ └─┘  └┘
txt      └───────┘ └─┘  └┘
par      └───────┘ └─┘  └┘
pid               └─┘  
st   ─────────────────────┘└─
130      { simp only [h, dif_pos],
id                      └─────┘
src        └─────────┘ └┘└─────┘
typ        └─────────┘└┘└─────┘
doc        └─────────┘ └┘       
txt        └─────────┘ └┘       
par        └─────────┘ └┘       
pid            └──┘└┘ └┘       
st   ─────┘└────────────────────┘└─
131        have : continuous (λx:ℝ, max x 0) := continuous_id.max continuous_const,
id                └────────┘        └─┘         └───────────────┘ └──────────────┘
src        └─────┘└────────┘  └┘ └┘└─┘ └─────┘└───────────────┘└──────────────┘
typ        └─────┘└────────┘  └┘ └┘└─┘ └─────┘└───────────────┘└──────────────┘
doc        └─────┘└────────┘  └┘ └┘    └─────┘                 
txt        └─────┘            └┘ └┘    └─────┘                 
par        └─────┘            └┘ └┘    └─────┘                 
pid        └───┘└┘            └┘ └┘    └─┘└──┘                 
st   ────────────────────────────────────────────────────────────────────────────┘└─
132        exact this.comp (continuous_apply 0) },
id               └───────┘  └──────────────┘
src        └────┘└───────┘ └──────────────┘└──┘
typ        └────┘└───────┘ └──────────────┘└──┘
doc        └────┘                          └──┘
txt        └────┘                          └──┘
par        └────┘                          └──┘
pid                                       └─┘
st   ──────────────────────────────────────────┘└┘
133      { simp [h],
id               
src        └────┘ 
typ        └────┘
doc        └────┘ 
txt        └────┘ 
par        └────┘ 
pid             
st   ─────────────┘└─
134        exact continuous_apply i }
id               └──────────────┘ 
src        └────┘└──────────────┘ 
typ        └────┘└──────────────┘
doc        └────┘                 
txt        └────┘                 
par        └────┘                 
pid                              
st   ──────────────────────────────┘└─
135    end }
st   ────┘
136  
137  /--
138  Definition of the model with corners (euclidean_space n, euclidean_quadrant n), used as a
139  model for manifolds with corners -/
140  def model_with_corners_euclidean_quadrant (n : ℕ) :
id                                                  
src                                                 
typ                                                 
141    model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n) :=
id     └────────────────┘   └─────────────┘    └────────────────┘ 
src    └────────────────┘   └─────────────┘     └────────────────┘
typ    └────────────────┘   └─────────────┘    └────────────────┘ 
doc    └────────────────┘    └─────────────┘     └────────────────┘
142  { to_fun     := λx, x.val,
id                      └──┘
src                       └──┘
typ                     └──┘
143    inv_fun    := λx, ⟨λi, max (x i) 0,
id                          └─┘   
src                           └─┘
typ                         └─┘   
144                      λi, by simp [le_refl]⟩,
id                                   └─────┘
src                             └────┘└─────┘
typ                            └────┘└─────┘
doc                             └────┘       
txt                             └────┘       
par                             └────┘       
pid                                        
st                             └─────────────┘
145    source     := univ,
id                   └──┘
src                  └──┘
typ                  └──┘
146    target     := range (λx : euclidean_quadrant n, x.val),
id                   └───┘       └────────────────┘   └──┘
src                  └───┘       └────────────────┘     └──┘
typ                  └───┘       └────────────────┘   └──┘
doc                  └───┘       └────────────────┘
147    map_source := λx hx, by simpa [-mem_range, mem_range_self] using x.property,
id                     └┘                        └────────────┘        └────────┘
src                            └─────────────────┘└────────────┘└──────┘└────────┘
typ                    └┘     └─────────────────┘└────────────┘└──────┘└────────┘
doc                            └─────────────────┘              └──────┘
txt                            └─────────────────┘              └──────┘
par                            └─────────────────┘              └──────┘
pid                                 └───────────┘              └────┘
st                            └──────────────────────────────────────────────────┘
148    map_target := λx hx, mem_univ _,
id                     └┘  └──────┘
src                         └──────┘
typ                    └┘  └──────┘
149    left_inv   := λ⟨xval, xprop⟩ hx, begin
id                                 └┘
typ                                └┘
st                                      └─────
150      rw subtype.mk_eq_mk,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────┘└─
151      ext1 i,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid          └┘
st   ─────────┘└─
152      simp [xprop i]
id             └───┘ 
src      └────┘      └─
typ      └────┘└───┘└─
doc      └────┘      └─
txt      └────┘      └─
par      └────┘      └─
pid                
st   ───────────────────
153    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
154    right_inv := λx hx, begin
id                    └┘
typ                   └┘
st                         └─────
155      rw range_quadrant at hx,
id          └────────────┘
src      └─┘└────────────┘└────┘
typ      └─┘└────────────┘└────┘
doc      └─┘              └────┘
txt      └─┘              └────┘
par      └─┘              └────┘
pid                      └────┘
st   ──────────────────────────┘└─
156      ext1 i,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid          └┘
st   ─────────┘└─
157      simp [hx i]
id             └┘ 
src      └────┘   └─
typ      └────┘└┘└─
doc      └────┘   └─
txt      └────┘   └─
par      └────┘   └─
pid             
st   ────────────────
158    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
159    source_eq   := rfl,
id                    └─┘
src                   └─┘
typ                   └─┘
160    unique_diff := begin
st                    └─────
161      /- To check that the quadrant has the unique differentiability property, we use the criterion
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
162      `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
163      rw range_quadrant,
id          └────────────┘
src      └─┘└────────────┘
typ      └─┘└────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────┘└─
164      apply unique_diff_on_convex,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘└───────────────────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
165      show convex {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i},
id            └────┘     └─────────────┘            └─┘      
src      └───┘└────┘└──┘└─────────────┘ └─┘ └────┘└─┘  └─┘  
typ      └───┘└────┘└──┘└─────────────┘ └─┘ └────┘└─┘ └─┘  
doc      └───┘└────┘ └──┘└─────────────┘ └─┘ └────┘     └─┘   
txt      └───┘       └──┘                └─┘ └────┘     └─┘   
par      └───┘       └──┘                └─┘ └────┘     └─┘   
pid      └───┘       └──┘                └─┘ └────┘     └─┘   
st   ───────────────────────────────────────────────────────────────┘└─
166      { assume x y hx hy a b ha hb hab i,
src        └──────────────────────────────┘
typ        └──────────────────────────────┘
doc        └──────────────────────────────┘
txt        └──────────────────────────────┘
par        └──────────────────────────────┘
pid        └──────────────────────────────┘
st   ─────┘└──────────────────────────────┘└─
167        simpa using add_le_add (mul_nonneg' ha (hx i)) (mul_nonneg' hb (hy i)) },
id                     └────────┘              └┘  └┘      └─────────┘ └┘  └┘ 
src        └──────────┘└────────┘                  └─┘ └─────────┘      └─┘
typ        └──────────┘└────────┘            └┘ └┘ └─┘ └─────────┘└┘ └┘└─┘
doc        └──────────┘                            └─┘                  └─┘
txt        └──────────┘                            └─┘                  └─┘
par        └──────────┘                            └─┘                  └─┘
pid             └────┘                            └─┘                  └┘
st   ────────────────────────────────────────────────────────────────────────────┘└┘
168      show (interior {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i}).nonempty,
id             └──────┘     └─────────────┘            └─┘ 
src      └───┘ └──────┘└──┘└─────────────┘ └─┘ └────┘└─┘  └─┘   └─────────┘
typ      └───┘ └──────┘└──┘└─────────────┘ └─┘ └────┘└─┘ └─┘   └─────────┘
doc      └───┘ └──────┘ └──┘└─────────────┘ └─┘ └────┘     └─┘   └─────────┘
txt      └───┘          └──┘                └─┘ └────┘     └─┘   └─────────┘
par      └───┘          └──┘                └─┘ └────┘     └─┘   └─────────┘
pid      └───┘          └──┘                └─┘ └────┘     └─┘   └────────┘
st   ───────────────────────────────────────────────────────────────────────────────
169      { use (λi, 1),
src        └──┘  └───┘
typ        └──┘  └───┘
doc        └──┘  └───┘
txt        └──┘  └───┘
par        └──┘  └───┘
pid             └───┘
st   ────────────────┘└─
170        rw mem_interior,
id            └──────────┘
src        └─┘└──────────┘
typ        └─┘└──────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────────────┘└─
171        refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,
id                  └┘  └──┘        └─┘          └─┘     └─┘
src        └─────┘  └┘ └──┘└─┘    └─┘ └─┘  └─┘ └─┘└───┘└─┘ └───────
typ        └─────┘  └┘ └──┘└─┘    └─┘└─┘  └─┘ └─┘└───┘└─┘ └───────
doc        └─────┘  └┘     └─┘        └─┘  └─┘ └─┘└───┘    └───────
txt        └─────┘         └─┘        └─┘  └─┘    └───┘    └───────
par        └─────┘         └─┘        └─┘  └─┘    └───┘    └───────
pid                       └─┘        └─┘  └─┘    └───┘    └───────
st   ──────────────────────────────────────────────────────────────────
172          is_open_set_pi finite_univ (λa ha, is_open_Ioi), _⟩,
id           └────────────┘ └─────────┘         └─────────┘
src  ───────┘└────────────┘└─────────┘  └────┘└─────────┘└───┘
typ  ───────┘└────────────┘└─────────┘  └────┘└─────────┘└───┘
doc  ───────┘                           └────┘           └───┘
txt  ───────┘                           └────┘           └───┘
par  ───────┘                           └────┘           └───┘
pid  ───────┘                           └────┘           └───┘
st   ──────────────────────────────────────────────────────────┘└─
173        { assume x hx i,
src          └───────────┘
typ          └───────────┘
doc          └───────────┘
txt          └───────────┘
par          └───────────┘
pid          └───────────┘
st   ───────┘└───────────┘└─
174          simp [pi] at hx,
id                 └┘
src          └────┘└┘└─────┘
typ          └────┘└┘└─────┘
doc          └────┘└┘└─────┘
txt          └────┘  └─────┘
par          └────┘  └─────┘
pid                └───┘
st   ──────────────────────┘└─
175          exact le_of_lt (hx i) },
id                 └──────┘  └┘ 
src          └────┘└──────┘    └┘
typ          └────┘└──────┘ └┘└┘
doc          └────┘            └┘
txt          └────┘            └┘
par          └────┘            └┘
pid                           
st   ─────────────────────────────┘└┘
176        { simp only [pi, forall_prop_of_true, mem_univ, mem_Ioi],
id                      └┘  └─────────────────┘  └──────┘  └─────┘
src          └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘
typ          └─────────┘└┘└┘└─────────────────┘└┘└──────┘└┘└─────┘
doc          └─────────┘└┘└┘                   └┘        └┘       
txt          └─────────┘  └┘                   └┘        └┘       
par          └─────────┘  └┘                   └┘        └┘       
pid              └──┘└┘  └┘                   └┘        └┘       
st   ─────────────────────────────────────────────────────────────┘└─
177          assume i,
src          └──────┘
typ          └──────┘
doc          └──────┘
txt          └──────┘
par          └──────┘
pid          └──────┘
st   ───────────────┘└─
178          exact zero_lt_one } }
id                 └─────────┘
src          └────┘└─────────┘
typ          └────┘└─────────┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                          
st   ─────────────────────────┘└───
179    end,
st   ────┘
180    continuous_to_fun  := continuous_subtype_val,
id                           └────────────────────┘
src                          └────────────────────┘
typ                          └────────────────────┘
181    continuous_inv_fun := begin
st                           └─────
182      apply continuous_subtype_mk,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
183      apply continuous_pi,
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────┘└─
184      assume i,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
185      have : continuous (λx:ℝ, max x 0) := continuous.max continuous_id continuous_const,
id              └────────┘        └─┘         └────────────┘ └───────────┘ └──────────────┘
src      └─────┘└────────┘  └┘ └┘└─┘ └─────┘└────────────┘└───────────┘└──────────────┘
typ      └─────┘└────────┘  └┘ └┘└─┘ └─────┘└────────────┘└───────────┘└──────────────┘
doc      └─────┘└────────┘  └┘ └┘    └─────┘                           
txt      └─────┘            └┘ └┘    └─────┘                           
par      └─────┘            └┘ └┘    └─────┘                           
pid      └───┘└┘            └┘ └┘    └─┘└──┘                           
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
186      exact this.comp (continuous_apply i)
id             └───────┘  └──────────────┘ 
src      └────┘└───────┘ └──────────────┘ └─
typ      └────┘└───────┘ └──────────────┘└─
doc      └────┘                           └─
txt      └────┘                           └─
par      └────┘                           └─
pid                                      
st   ─────────────────────────────────────────
187    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
188  
189  /--
190  Dummy class to make an assumption such as `x < y` available to typeclass search. Such an
191  assumption is used to define a manifold structure on [x, y] when `x < y`. Should be fixed in Lean 4.
192  -/
193  def lt_class {α : Type*} [has_lt α] (x y : α) : Prop := x < y
id                             └────┘                        
src                            └────┘                          
typ                            └────┘                        
194  attribute [class] lt_class
id                     └──────┘
src                    └──────┘
typ                    └──────┘
doc                    └──────┘
195  
196  /--
197  The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in
198  `euclidean_half_space 1`.
199  -/
200  def Icc_left_chart (x y : ℝ) [h : lt_class x y] :
id                                    └──────┘  
src                                   └──────┘
typ                                   └──────┘  
doc                                    └──────┘
201    local_homeomorph (Icc x y) (euclidean_half_space 1) :=
id     └──────────────┘  └─┘     └──────────────────┘
src    └──────────────┘  └─┘       └──────────────────┘
typ    └──────────────┘  └─┘     └──────────────────┘
doc    └──────────────┘  └─┘       └──────────────────┘
202  { source := {z : Icc x y | z.val < y},
id                   └─┘     └──┘  
src                  └─┘        └──┘ 
typ                  └─┘     └──┘  
doc                   └─┘
203    target := {z : euclidean_half_space 1 | z.val 0 < y - x},
id                   └──────────────────┘     └──┘      
src                  └──────────────────┘      └──┘      
typ                  └──────────────────┘     └──┘      
doc                   └──────────────────┘
204    to_fun := λ(z : Icc x y), ⟨λi, z.val - x, sub_nonneg.mpr z.property.1⟩,
id                     └─┘         └──┘    └────────┘└──┘ └───────┘
src                    └─┘             └──┘     └────────┘└──┘  └───────┘
typ                    └─┘         └──┘    └────────┘└──┘ └───────┘
doc                    └─┘
205    inv_fun := λz, ⟨min (z.val 0 + x) y, by simp [le_refl, z.property, le_of_lt h]⟩,
id                    └─┘  └──┘                 └─────┘              └──────┘ 
src                    └─┘   └──┘             └────┘└─────┘└┘          └┘└──────┘ 
typ                   └─┘  └──┘           └────┘└─────┘└┘└────────┘└┘└──────┘
doc                                            └────┘       └┘          └┘         
txt                                            └────┘       └┘          └┘         
par                                            └────┘       └┘          └┘         
pid                                                       └┘          └┘         
st                                            └─────────────────────────────────────┘
206    map_source := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
207    map_target := by { simp, assume z hz, left, linarith },
src                       └──┘  └─────────┘  └──┘  └───────┘
typ                       └──┘  └─────────┘  └──┘  └───────┘
doc                       └──┘  └─────────┘  └──┘  └───────┘
txt                       └──┘  └─────────┘  └──┘  └───────┘
par                       └──┘  └─────────┘  └──┘  └───────┘
pid                             └─────────┘                
st                     └─────┘└───────────┘└────┘└─────────┘└┘
208    left_inv := by { rintros ⟨z, hz⟩ h'z, simp at hz h'z, simp [hz, h'z] },
id                                                                 └┘  └─┘
src                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
typ                     └─────────────────┘  └────────────┘  └────┘└┘└┘└─┘└┘
doc                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
txt                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
par                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
pid                            └──────────┘      └───────┘        └┘   
st                   └────────────────────┘└──────────────┘└───────────────┘└┘
209    right_inv := begin
st                  └─────
210      rintros ⟨z, hz⟩ h'z,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid             └──────────┘
st   ──────────────────────┘└─
211      rw subtype.mk_eq_mk,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────┘└─
212      funext,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
st   ─────────┘└─
213      simp at hz h'z,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid          └───────┘
st   ─────────────────┘└─
214      have A : x + z 0 ≤ y, by linarith,
id                       
src      └───────┘   └─┘      └──────┘
typ      └───────┘ └─┘     └──────┘
doc      └───────┘   └─┘       └──────┘
txt      └───────┘   └─┘       └──────┘
par      └───────┘   └─┘       └──────┘
pid      └────┘└─┘   └─┘ 
st   ───────────────────────┘             └─
215      rw subsingleton.elim i 0,
id          └───────────────┘ 
src      └─┘└───────────────┘ └┘
typ      └─┘└───────────────┘└┘
doc      └─┘                  └┘
txt      └─┘                  └┘
par      └─┘                  └┘
pid                          
st   ──────────────────────────────
216      simp [A],
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid           
st   ───────────┘└─
217    end,
st   ────┘
218    open_source := begin
st                    └─────
219      have : is_open {z : ℝ | z < y} := is_open_Iio,
id              └─────┘                  └─────────┘
src      └─────┘└─────┘└──┘ └─┘   └───┘└─────────┘
typ      └─────┘└─────┘└──┘ └─┘  └───┘└─────────┘
doc      └─────┘└─────┘ └──┘ └─┘   └───┘
txt      └─────┘        └──┘ └─┘   └───┘
par      └─────┘        └──┘ └─┘   └───┘
pid      └───┘└┘        └──┘ └─┘   └──┘
st   ────────────────────────────────────────────────┘└─
220      exact continuous_subtype_val _ this
id             └────────────────────┘   └──┘
src      └────┘└────────────────────┘└─┘    
typ      └────┘└────────────────────┘└─┘└──┘
doc      └────┘                      └─┘    
txt      └────┘                      └─┘    
par      └────┘                      └─┘    
pid                                 └─┘    
st   ────────────────────────────────────────
221    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
222    open_target := begin
st                    └─────
223      have : is_open {z : ℝ | z < y - x} := is_open_Iio,
id              └─────┘                    └─────────┘
src      └─────┘└─────┘└──┘ └─┘    └───┘└─────────┘
typ      └─────┘└─────┘└──┘ └─┘  └───┘└─────────┘
doc      └─────┘└─────┘ └──┘ └─┘     └───┘
txt      └─────┘        └──┘ └─┘     └───┘
par      └─────┘        └──┘ └─┘     └───┘
pid      └───┘└┘        └──┘ └─┘     └──┘
st   ────────────────────────────────────────────────────┘└─
224      have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
id              └─────┘     └─┘                 
src      └─────┘└─────┘└──┘└─┘└─┘  └─┘ └─┘    └────
typ      └─────┘└─────┘└──┘└─┘└─┘ └─┘ └─┘  └────
doc      └─────┘└─────┘ └──┘   └─┘  └─┘ └─┘    └────
txt      └─────┘        └──┘   └─┘  └─┘ └─┘    └────
par      └─────┘        └──┘   └─┘  └─┘ └─┘    └────
pid      └───┘└┘        └──┘   └─┘  └─┘ └─┘    └───
st   ────────────────────────────────────────────────────
225        (continuous_apply 0) _ this,
id          └──────────────┘      └──┘
src  ─────┘ └──────────────┘└────┘
typ  ─────┘ └──────────────┘└────┘└──┘
doc  ─────┘                 └────┘
txt  ─────┘                 └────┘
par  ─────┘                 └────┘
pid  ─────┘                 └────┘
st   ────────────────────────────────┘└─
226      exact continuous_subtype_val _ this
id             └────────────────────┘   └──┘
src      └────┘└────────────────────┘└─┘    
typ      └────┘└────────────────────┘└─┘└──┘
doc      └────┘                      └─┘    
txt      └────┘                      └─┘    
par      └────┘                      └─┘    
pid                                 └─┘    
st   ────────────────────────────────────────
227    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
228    continuous_to_fun := begin
st                          └─────
229      apply continuous.continuous_on,
id             └──────────────────────┘
src      └────┘└──────────────────────┘
typ      └────┘└──────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────┘└─
230      apply continuous_subtype_mk,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
231      have : continuous (λ (z : ℝ) (i : fin 1), z - x) :=
id              └────────┘                 └─┘         
src      └─────┘└────────┘  └────┘ └─────┘└─┘└───┘   └────
typ      └─────┘└────────┘  └────┘ └─────┘└─┘└───┘  └────
doc      └─────┘└────────┘  └────┘ └─────┘   └───┘   └────
txt      └─────┘            └────┘ └─────┘   └───┘   └────
par      └─────┘            └────┘ └─────┘   └───┘   └────
pid      └───┘└┘            └────┘ └─────┘   └───┘   └───
st   ────────────────────────────────────────────────────────
232        continuous.sub (continuous_pi $ λi, continuous_id) continuous_const,
id         └────────────┘  └───────────┘       └───────────┘  └──────────────┘
src  ─────┘└────────────┘ └───────────┘  └─┘└───────────┘└┘└──────────────┘
typ  ─────┘└────────────┘ └───────────┘  └─┘└───────────┘└┘└──────────────┘
doc  ─────┘                              └─┘             └┘
txt  ─────┘                              └─┘             └┘
par  ─────┘                              └─┘             └┘
pid  ─────┘                              └─┘             └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
233      exact this.comp continuous_subtype_val,
id             └───────┘ └────────────────────┘
src      └────┘└───────┘└────────────────────┘
typ      └────┘└───────┘└────────────────────┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ─────────────────────────────────────────┘└─
234    end,
st   ────┘
235    continuous_inv_fun := begin
st                           └─────
236      apply continuous.continuous_on,
id             └──────────────────────┘
src      └────┘└──────────────────────┘
typ      └────┘└──────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────┘└─
237      apply continuous_subtype_mk,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
238      have A : continuous (λ z : ℝ, min (z + x) y) :=
id                └────────┘           └─┘        
src      └───────┘└────────┘  └───┘ └┘└─┘    └┘ └────
typ      └───────┘└────────┘  └───┘ └┘└─┘   └┘└────
doc      └───────┘└────────┘  └───┘ └┘       └┘ └────
txt      └───────┘            └───┘ └┘       └┘ └────
par      └───────┘            └───┘ └┘       └┘ └────
pid      └────┘└─┘            └───┘ └┘       └┘ └───
st   ────────────────────────────────────────────────────
239        (continuous_id.add continuous_const).min continuous_const,
id          └───────────────┘                       └──────────────┘
src  ─────┘ └───────────────┘                └────┘└──────────────┘
typ  ─────┘ └───────────────┘                └────┘└──────────────┘
doc  ─────┘                                  └────┘
txt  ─────┘                                  └────┘
par  ─────┘                                  └────┘
pid  ─────┘                                  └────┘
st   ──────────────────────────────────────────────────────────────┘└─
240      have B : continuous (λz : fin 1 → ℝ, z 0) := continuous_apply 0,
id                └────────┘       └─┘                └──────────────┘
src      └───────┘└────────┘  └──┘└─┘└─┘  └┘ └─────┘└──────────────┘└┘
typ      └───────┘└────────┘  └──┘└─┘└─┘  └┘ └─────┘└──────────────┘└┘
doc      └───────┘└────────┘  └──┘   └─┘  └┘ └─────┘                └┘
txt      └───────┘            └──┘   └─┘  └┘ └─────┘                └┘
par      └───────┘            └──┘   └─┘  └┘ └─────┘                └┘
pid      └────┘└─┘            └──┘   └─┘  └┘ └─┘└──┘                
st   ──────────────────────────────────────────────────────────────────┘└─
241      exact (A.comp B).comp continuous_subtype_val
id              └────┘        └────────────────────┘
src      └────┘ └────┘ └─────┘└────────────────────┘
typ      └────┘ └────┘└─────┘└────────────────────┘
doc      └────┘        └─────┘                      
txt      └────┘        └─────┘                      
par      └────┘        └─────┘                      
pid                   └─────┘                      
st   ─────────────────────────────────────────────────
242    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
243  
244  /--
245  The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in
246  `euclidean_half_space 1`.
247  -/
248  def Icc_right_chart (x y : ℝ) [h : lt_class x y] :
id                                     └──────┘  
src                                    └──────┘
typ                                    └──────┘  
doc                                     └──────┘
249    local_homeomorph (Icc x y) (euclidean_half_space 1) :=
id     └──────────────┘  └─┘     └──────────────────┘
src    └──────────────┘  └─┘       └──────────────────┘
typ    └──────────────┘  └─┘     └──────────────────┘
doc    └──────────────┘  └─┘       └──────────────────┘
250  { source := {z : Icc x y | x < z.val},
id                   └─┘       └──┘
src                  └─┘           └──┘
typ                  └─┘       └──┘
doc                   └─┘
251    target := {z : euclidean_half_space 1 | z.val 0 < y - x},
id                   └──────────────────┘     └──┘      
src                  └──────────────────┘      └──┘      
typ                  └──────────────────┘     └──┘      
doc                   └──────────────────┘
252    to_fun := λ(z : Icc x y), ⟨λi, y - z.val, sub_nonneg.mpr z.property.2⟩,
id                     └─┘           └──┘  └────────┘└──┘ └───────┘
src                    └─┘                └──┘  └────────┘└──┘  └───────┘
typ                    └─┘           └──┘  └────────┘└──┘ └───────┘
doc                    └─┘
253    inv_fun := λz, ⟨max (y - z.val 0) x, by simp [le_refl, z.property, le_of_lt h]⟩,
id                    └─┘    └──┘               └─────┘              └──────┘ 
src                    └─┘      └──┘          └────┘└─────┘└┘          └┘└──────┘ 
typ                   └─┘    └──┘         └────┘└─────┘└┘└────────┘└┘└──────┘
doc                                            └────┘       └┘          └┘         
txt                                            └────┘       └┘          └┘         
par                                            └────┘       └┘          └┘         
pid                                                       └┘          └┘         
st                                            └─────────────────────────────────────┘
254    map_source := by simp,
src                     └──┘
typ                     └──┘
doc                     └──┘
txt                     └──┘
par                     └──┘
st                     └───┘
255    map_target := by { simp, assume z hz, left, linarith },
src                       └──┘  └─────────┘  └──┘  └───────┘
typ                       └──┘  └─────────┘  └──┘  └───────┘
doc                       └──┘  └─────────┘  └──┘  └───────┘
txt                       └──┘  └─────────┘  └──┘  └───────┘
par                       └──┘  └─────────┘  └──┘  └───────┘
pid                             └─────────┘                
st                     └─────┘└───────────┘└────┘└─────────┘└┘
256    left_inv := by { rintros ⟨z, hz⟩ h'z, simp at hz h'z, simp [hz, h'z] },
id                                                                 └┘  └─┘
src                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
typ                     └─────────────────┘  └────────────┘  └────┘└┘└┘└─┘└┘
doc                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
txt                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
par                     └─────────────────┘  └────────────┘  └────┘  └┘   └┘
pid                            └──────────┘      └───────┘        └┘   
st                   └────────────────────┘└──────────────┘└───────────────┘└┘
257    right_inv := begin
st                  └─────
258      rintros ⟨z, hz⟩ h'z,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid             └──────────┘
st   ──────────────────────┘└─
259      rw subtype.mk_eq_mk,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────┘└─
260      funext,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
st   ─────────┘└─
261      simp at hz h'z,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid          └───────┘
st   ─────────────────┘└─
262      have A : x ≤ y + -z 0, by linarith,
id                      
src      └───────┘     └┘     └──────┘
typ      └───────┘  └┘     └──────┘
doc      └───────┘      └┘     └──────┘
txt      └───────┘      └┘     └──────┘
par      └───────┘      └┘     └──────┘
pid      └────┘└─┘      
st   ────────────────────────┘             └─
263      rw subsingleton.elim i 0,
id          └───────────────┘ 
src      └─┘└───────────────┘ └┘
typ      └─┘└───────────────┘└┘
doc      └─┘                  └┘
txt      └─┘                  └┘
par      └─┘                  └┘
pid                          
st   ──────────────────────────────
264      simp [A],
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid           
st   ───────────┘└─
265    end,
st   ────┘
266    open_source := begin
st                    └─────
267      have : is_open {z : ℝ | x < z} := is_open_Ioi,
id              └─────┘                  └─────────┘
src      └─────┘└─────┘└──┘ └─┘   └───┘└─────────┘
typ      └─────┘└─────┘└──┘ └─┘  └───┘└─────────┘
doc      └─────┘└─────┘ └──┘ └─┘   └───┘
txt      └─────┘        └──┘ └─┘   └───┘
par      └─────┘        └──┘ └─┘   └───┘
pid      └───┘└┘        └──┘ └─┘   └──┘
st   ────────────────────────────────────────────────┘└─
268      exact continuous_subtype_val _ this
id             └────────────────────┘   └──┘
src      └────┘└────────────────────┘└─┘    
typ      └────┘└────────────────────┘└─┘└──┘
doc      └────┘                      └─┘    
txt      └────┘                      └─┘    
par      └────┘                      └─┘    
pid                                 └─┘    
st   ────────────────────────────────────────
269    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
270    open_target := begin
st                    └─────
271      have : is_open {z : ℝ | z < y - x} := is_open_Iio,
id              └─────┘                    └─────────┘
src      └─────┘└─────┘└──┘ └─┘    └───┘└─────────┘
typ      └─────┘└─────┘└──┘ └─┘  └───┘└─────────┘
doc      └─────┘└─────┘ └──┘ └─┘     └───┘
txt      └─────┘        └──┘ └─┘     └───┘
par      └─────┘        └──┘ └─┘     └───┘
pid      └───┘└┘        └──┘ └─┘     └──┘
st   ────────────────────────────────────────────────────┘└─
272      have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
id              └─────┘     └─┘                 
src      └─────┘└─────┘└──┘└─┘└─┘  └─┘ └─┘    └────
typ      └─────┘└─────┘└──┘└─┘└─┘ └─┘ └─┘  └────
doc      └─────┘└─────┘ └──┘   └─┘  └─┘ └─┘    └────
txt      └─────┘        └──┘   └─┘  └─┘ └─┘    └────
par      └─────┘        └──┘   └─┘  └─┘ └─┘    └────
pid      └───┘└┘        └──┘   └─┘  └─┘ └─┘    └───
st   ────────────────────────────────────────────────────
273        (continuous_apply 0) _ this,
id          └──────────────┘      └──┘
src  ─────┘ └──────────────┘└────┘
typ  ─────┘ └──────────────┘└────┘└──┘
doc  ─────┘                 └────┘
txt  ─────┘                 └────┘
par  ─────┘                 └────┘
pid  ─────┘                 └────┘
st   ────────────────────────────────┘└─
274      exact continuous_subtype_val _ this
id             └────────────────────┘   └──┘
src      └────┘└────────────────────┘└─┘    
typ      └────┘└────────────────────┘└─┘└──┘
doc      └────┘                      └─┘    
txt      └────┘                      └─┘    
par      └────┘                      └─┘    
pid                                 └─┘    
st   ────────────────────────────────────────
275    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
276    continuous_to_fun := begin
277      apply continuous.continuous_on,
278      apply continuous_subtype_mk,
st                                  └─
279      have : continuous (λ (z : ℝ) (i : fin 1), y - z) :=
id              └────────┘                 └─┘     
src      └─────┘└────────┘  └────┘ └─────┘└─┘└───┘   └────
typ      └─────┘└────────┘  └────┘ └─────┘└─┘└───┘  └────
doc      └─────┘└────────┘  └────┘ └─────┘   └───┘   └────
txt      └─────┘            └────┘ └─────┘   └───┘   └────
par      └─────┘            └────┘ └─────┘   └───┘   └────
pid      └───┘└┘            └────┘ └─────┘   └───┘   └───
st   ────────────────────────────────────────────────────────
280        continuous_const.sub (continuous_pi (λi, continuous_id)),
id         └──────────────────┘  └───────────┘      └───────────┘
src  ─────┘└──────────────────┘ └───────────┘  └─┘└───────────┘└┘
typ  ─────┘└──────────────────┘ └───────────┘  └─┘└───────────┘└┘
doc  ─────┘                                    └─┘             └┘
txt  ─────┘                                    └─┘             └┘
par  ─────┘                                    └─┘             └┘
pid  ─────┘                                    └─┘             └┘
st   ─────────────────────────────────────────────────────────────┘└─
281      exact this.comp continuous_subtype_val,
id             └───────┘ └────────────────────┘
src      └────┘└───────┘└────────────────────┘
typ      └────┘└───────┘└────────────────────┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ─────────────────────────────────────────┘└─
282    end,
st   ────┘
283    continuous_inv_fun := begin
284      apply continuous.continuous_on,
285      apply continuous_subtype_mk,
st                                  └─
286      have A : continuous (λ z : ℝ, max (y - z) x) :=
id                └────────┘           └─┘        
src      └───────┘└────────┘  └───┘ └┘└─┘    └┘ └────
typ      └───────┘└────────┘  └───┘ └┘└─┘   └┘└────
doc      └───────┘└────────┘  └───┘ └┘       └┘ └────
txt      └───────┘            └───┘ └┘       └┘ └────
par      └───────┘            └───┘ └┘       └┘ └────
pid      └────┘└─┘            └───┘ └┘       └┘ └───
st   ────────────────────────────────────────────────────
287        (continuous_const.sub continuous_id).max continuous_const,
id          └──────────────────┘ └───────────┘      └──────────────┘
src  ─────┘ └──────────────────┘└───────────┘└────┘└──────────────┘
typ  ─────┘ └──────────────────┘└───────────┘└────┘└──────────────┘
doc  ─────┘                                  └────┘
txt  ─────┘                                  └────┘
par  ─────┘                                  └────┘
pid  ─────┘                                  └────┘
st   ──────────────────────────────────────────────────────────────┘└─
288      have B : continuous (λz : fin 1 → ℝ, z 0) := continuous_apply 0,
id                └────────┘       └─┘                └──────────────┘
src      └───────┘└────────┘  └──┘└─┘└─┘  └┘ └─────┘└──────────────┘└┘
typ      └───────┘└────────┘  └──┘└─┘└─┘  └┘ └─────┘└──────────────┘└┘
doc      └───────┘└────────┘  └──┘   └─┘  └┘ └─────┘                └┘
txt      └───────┘            └──┘   └─┘  └┘ └─────┘                └┘
par      └───────┘            └──┘   └─┘  └┘ └─────┘                └┘
pid      └────┘└─┘            └──┘   └─┘  └┘ └─┘└──┘                
st   ──────────────────────────────────────────────────────────────────┘└─
289      exact (A.comp B).comp continuous_subtype_val
id              └────┘        └────────────────────┘
src      └────┘ └────┘ └─────┘└────────────────────┘
typ      └────┘ └────┘└─────┘└────────────────────┘
doc      └────┘        └─────┘                      
txt      └────┘        └─────┘                      
par      └────┘        └─────┘                      
pid                   └─────┘                      
st   ─────────────────────────────────────────────────
290    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
291  
292  /--
293  Manifold with boundary structure on [x, y], using only two charts.
294  -/
295  instance Icc_manifold (x y : ℝ) [h : lt_class x y] : manifold (euclidean_half_space 1) (Icc x y) :=
id                                       └──────┘      └──────┘  └──────────────────┘     └─┘  
src                                      └──────┘        └──────┘  └──────────────────┘     └─┘
typ                                      └──────┘      └──────┘  └──────────────────┘     └─┘  
doc                                       └──────┘        └──────┘  └──────────────────┘     └─┘
296  { atlas := {Icc_left_chart x y, Icc_right_chart x y},
id              └────────────┘   └─────────────┘  
src             └────────────┘     └─────────────┘
typ             └────────────┘   └─────────────┘  
doc              └────────────┘      └─────────────┘
297    chart_at := λz, if z.val < y then Icc_left_chart x y else Icc_right_chart x y,
id                       └──┘        └────────────┘        └─────────────┘  
src                        └──┘         └────────────┘          └─────────────┘
typ                      └──┘        └────────────┘        └─────────────┘  
doc                                      └────────────┘          └─────────────┘
298    mem_chart_source := λz, begin
id                          
typ                         
st                             └─────
299      by_cases h' : z.val < y,
id                     └───┘  
src      └───────┘  └─┘└───┘
typ      └───────┘  └─┘└───┘
doc      └───────┘  └─┘      
txt      └───────┘  └─┘      
par      └───────┘  └─┘      
pid                └─┘      
st   ──────────────────────────┘└─
300      { simp only [h', if_true],
id                    └┘  └─────┘
src        └─────────┘  └┘└─────┘
typ        └─────────┘└┘└┘└─────┘
doc        └─────────┘  └┘       
txt        └─────────┘  └┘       
par        └─────────┘  └┘       
pid            └──┘└┘  └┘       
st   ─────┘└─────────────────────┘└─
301        exact h' },
id               └┘
src        └────┘  
typ        └────┘└┘
doc        └────┘  
txt        └────┘  
par        └────┘  
pid               
st   ──────────────┘└┘
302      { simp only [h', if_false],
id                    └┘  └──────┘
src        └─────────┘  └┘└──────┘
typ        └─────────┘└┘└┘└──────┘
doc        └─────────┘  └┘        
txt        └─────────┘  └┘        
par        └─────────┘  └┘        
pid            └──┘└┘  └┘        
st   ─────────────────────────────┘└─
303        apply lt_of_lt_of_le h,
id               └────────────┘ 
src        └────┘└────────────┘
typ        └────┘└────────────┘
doc        └────┘              
txt        └────┘              
par        └────┘              
pid                           
st   ───────────────────────────┘└─
304        simpa using h' }
id                     └┘
src        └──────────┘  
typ        └──────────┘└┘
doc        └──────────┘  
txt        └──────────┘  
par        └──────────┘  
pid             └────┘  
st   ────────────────────┘└─
305    end,
st   ────┘
306    chart_mem_atlas := λz, by { by_cases h' : z.val < y; simp [h'] } }
id                                              └───┘           └┘
src                                └───────┘  └─┘└───┘    └────┘  └┘
typ                               └───────┘  └─┘└───┘   └────┘└┘└┘
doc                                └───────┘  └─┘         └────┘  └┘
txt                                └───────┘  └─┘         └────┘  └┘
par                                └───────┘  └─┘         └────┘  └┘
pid                                          └─┘               
st                              └────────────────────────────────────┘└┘
307  
308  /--
309  The manifold structure on [x, y] is smooth.
310  -/
311  instance Icc_smooth_manifold (x y : ℝ) [lt_class x y] :
id                                          └──────┘  
src                                         └──────┘
typ                                         └──────┘  
doc                                          └──────┘
312    smooth_manifold_with_corners (model_with_corners_euclidean_half_space 1) (Icc x y) :=
id     └──────────────────────────┘  └─────────────────────────────────────┘     └─┘  
src    └──────────────────────────┘  └─────────────────────────────────────┘     └─┘
typ    └──────────────────────────┘  └─────────────────────────────────────┘     └─┘  
doc    └──────────────────────────┘  └─────────────────────────────────────┘     └─┘
313  begin
st   └─────
314    have M : times_cont_diff_on ℝ ⊤ (λz : fin 1 → ℝ, (λi : fin 1, y - x) - z) univ,
id              └────────────────┘          └─┘             └─┘             └──┘
src    └───────┘└────────────────┘   └──┘   └─┘  └┘  └──┘└─┘└──┘  └┘  └┘└──┘
typ    └───────┘└────────────────┘   └──┘└─┘└─┘ └┘  └──┘└─┘└──┘└┘  └┘└──┘
doc    └───────┘└────────────────┘    └──┘   └─┘  └┘  └──┘   └──┘   └┘  └┘
txt    └───────┘                      └──┘   └─┘  └┘  └──┘   └──┘   └┘  └┘
par    └───────┘                      └──┘   └─┘  └┘  └──┘   └──┘   └┘  └┘
pid    └────┘└─┘                      └──┘   └─┘  └┘  └──┘   └──┘   └┘  └┘
st   ───────────────────────────────────────────────────────────────────────────────┘└┘
315    { rw times_cont_diff_on_univ,
316      exact times_cont_diff.sub times_cont_diff_const times_cont_diff_id },
st                                                                          └┘
317    haveI : has_groupoid (Icc x y)
id                                
typ                               
318            (times_cont_diff_groupoid ⊤ (model_with_corners_euclidean_half_space 1)) :=
319    begin
320      apply has_groupoid_of_pregroupoid,
321      assume e e' he he',
322      simp [atlas] at he he',
323      /- We need to check that any composition of two charts gives a C^∞ function. Each chart can be
324      either the left chart or the right chart, leaving 4 possibilities that we handle successively.
325      -/
326      rcases he with rfl | rfl; rcases he' with rfl | rfl,
327      { -- e = right chart, e' = right chart
328        refine ((mem_groupoid_of_pregroupoid _ _).mpr _).1,
329        exact symm_trans_mem_times_cont_diff_groupoid _ _ _ },
st                                                             └┘
330      { -- e = right chart, e' = left chart
331        apply M.congr_mono _ _ (subset_univ _),
332        { rw inter_comm,
333          refine unique_diff_on.inter (model_with_corners.unique_diff _) _,
334          exact model_with_corners.continuous_inv_fun _ _ (local_homeomorph.open_source _) },
st                                                                                            └┘
335        { assume z hz,
336          simp [-mem_range, range_half_space, model_with_corners_euclidean_half_space,
337                local_equiv.trans_source, Icc_left_chart, Icc_right_chart] at hz,
338          have A : 0 ≤ z 0 := hz.2,
id                        
typ                       
339          have B : x ≤ y + -z 0, by { have := hz.1.1.1, linarith },
id                           
typ                          
st                                                                  └┘
340          have C : y + (-x + -z 0) = ((λ (i : fin 1), y + -x) + -z) 0,
id                                               └─┘         
src                                              └─┘
typ                                              └─┘         
341            by { change y + (-x - z 0) = (y - x) - z 0, ring },
id                                              
typ                                             
st                                                              └┘
342          ext i,
343          rw subsingleton.elim i 0,
id                                
typ                               
344          simpa [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, A, B] } },
st                                                                                                  └──┘
345      { -- e = left chart, e' = right chart
346        apply M.congr_mono _ _ (subset_univ _),
347        { rw inter_comm,
348          refine unique_diff_on.inter (model_with_corners.unique_diff _) _,
349          exact model_with_corners.continuous_inv_fun _ _ (local_homeomorph.open_source _) },
st                                                                                            └┘
350        { assume z hz,
351          simp [-mem_range, range_half_space, model_with_corners_euclidean_half_space,
352                local_equiv.trans_source, Icc_left_chart, Icc_right_chart] at hz,
353          have A : 0 ≤ z 0 := hz.2,
id                        
typ                       
354          have B : x + z 0 ≤ y, by { have := hz.1.1.1, linarith },
id                            
typ                           
st                                                                 └┘
355          have C : y + (-x + -z 0) = ((λ (i : fin 1), y + -x) + -z) 0,
id                                               └─┘         
src                                              └─┘
typ                                              └─┘         
356            by { change y + (-x - z 0) = (y - x) - z 0, ring },
id                                              
typ                                             
st                                                              └┘
357          ext i,
358          rw subsingleton.elim i 0,
id                                
typ                               
359          simpa [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, A, B] } },
st                                                                                                  └──┘
360      { -- e = left chart, e' = left chart
361        refine ((mem_groupoid_of_pregroupoid _ _).mpr _).1,
362        exact symm_trans_mem_times_cont_diff_groupoid _ _ _ }
st                                                             └┘
363    end,
st     └─┘
364    constructor
365  end
st   └─┘